$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $P$:($A$$\rightarrow\mathbb{B}$). $X$$\mid$$a$.$P$($a$) $\in$ AbsInterface($A$)